<div class="section1"><div class="Normal"><span style="" font-weight:="" bold="" font-style:="" italic="">Dr Jean-Pierre Jouannaud</span><span style="" font-style:="" italic="">, Prof of computers, Ecole Polytechnique Palaiseau, France, On applications of formal maths for software safety & internet security</span><br /><br /><span style="" font-weight:="" bold="">What is formal mathematics?</span><br /><br />You see, mathematics has always been informal until now.
We have formulated theories and then gone on to prove them as well. But it has always been other mathematicians who have checked them for validity. Leaving room for mistakes to take place. For it is human to err. That is where formal mathematics comes in. This is a recent attempt to formalise the notions of reasoning and computation in which the proof of a mathematical statement is itself proven to be correct via a calculation done on a computer. Even though the computer and softwares that check mathematical statement have been made by humans, the chance of errors in calculation are much lesser, in fact nil. <br /><br /><span style="" font-weight:="" bold="">What are its applications?</span><br /><br />Coq, the software that my colleagues and I have developed based on formal mathematics, is a very general one. It has to be used according to company needs to create specific solutions. This software has great use in telecommunications and the space industry. But currently, its main application is internet banking and security. Most people are turning to using ''smart cards'' these days and there are certain specific applications available on the card that work on this software.<br /><br /><span style="" font-weight:="" bold="">Does it have a future in India?</span><br /><br />It has a future anywhere as long as there is need for such software. And with so many banks coming onto the scene here, it surely will become popular in some time. Besides that there are so many good computer professionals in this country, all that is required is for companies to harness their talent in making much more sophisticated softwares using this one. <br /><br /><span style="" font-weight:="" bold="">How is it beneficial to your research if it is free?</span><br /><br />The only reason we are offering this software to companies free of cost is because we are generously funded by patrons all across Europe and of course by two institutes. Also, this way there is huge market that can be explored.</div> </div>